\newcommand{\newarr}{\longmapsto}
\newcommand{\newarro}[1]{\stackrel{#1}{\newarr}}

\subsection{A Finitely Branching LTS for \hof}\label{ss:lts}

In order to exploit the theory of well-structured transition systems, 
a finitely branching LTS for \hof is necessary.
This is not a significant requirement in our case; the sensible issue 
here is the treatment of alpha-conversion. 
To that end, 
we introduce an alternative LTS %$\newarro{\alpha}$ 
\emph{without} alpha-conversion. As we shall see, since 
we restrict ourselves to 
closed processes and proofs focus on internal synchronizations,
the finitely branching LTS is equivalent to that introduced in Section \ref{s:lang}.
The alternative LTS is given in Figure \ref{fig:newlts}; its most noticeable 
is the
absence of a side condition on rule \textsc{Act1}.


\begin{figure}[t]
\[
\mathrm{\textsc{Inp}}~~~{\inp a x. P} \stackrel{\ia a x  }{\newarr}   {P } \qquad \qquad \mathrm{\textsc{Out}}~~~{\Ho{a}{P}} \stackrel{\Ho a P  }{\newarr}  {\nil}\]
\[
\rightinfer	[\textsc{Act1}]
			{P_1 \parallel P_2 \stackrel{\alpha}{\newarr} P'_1 \parallel P_2}
			{P_1 \stackrel{\alpha}{\newarr} P_1' }
\qquad
\rightinfer	[\textsc{Tau1}]
			{P_1 \parallel P_2 \stackrel{\tau}{\newarr}  P'_1 \parallel P'_2 \sub{P}{x}}
			{P_1 \stackrel{\Ho{a}{P}}{\newarr} P_1' \andalso P_2 \stackrel{\iae a (x)}{\newarr} P'_2}
\]
\caption{A finitely branching LTS for \hof.
Rules \textsc{Act2} and \textsc{Tau2}, the symmetric counterparts of 
\textsc{Act1} and \textsc{Tau1}, have been omitted.
} \label{fig:newlts}
\end{figure}

%we are interested only in reduction semantics
%INTRO with justification

\begin{lemma}\label{lem:close}
 Let $P$ be a closed \hof process. For every $P'  \in \hof$ if $P \arro{~~} P'$ then $P'$ is a closed process.
\end{lemma}
\begin{proof}
By induction on the height of the inference tree for $P \arro{~~} P'$ considering the possible cases of the last step
of the inference. There are four cases, corresponding 
to those related to rules \textsc{Tau1}, \textsc{Tau2}, \textsc{Act1}, and \textsc{Act2}.
Let us focus only in the case in which 
 \textsc{Tau1} is the last rule applied; the other cases are similar or simpler. 
Then 
$P \equiv P_1 \parallel P_2$ with $P_1 \arro{~\outC{a}\langle R \rangle~} P'_1$
and $P_2 \arro{~a(x)~} P'_2$.
Hence $P_1 \equiv \outC{a}\langle R \rangle \parallel P'_1$ and
$P_2 \equiv a(x).P'_2$.
As such, 
%$P \equiv a(x).Q \parallel \Ho{a}{R}$ and 
$P' \equiv P'_1 \parallel P'_2 \sub{R}{x}$.
 We know that $P$ is a closed process; hence, 
both $P'_1$ and $R$ are closed processes, and $P'_2$ is an open process 
such that $\fn{P'_2} = \{x\}$.
%where the only free variable is $x$. 
Then the process $P'$ is closed since it is equivalent to the process $P'_2$ 
where all the free occurrences of the name $x$ has been replaced with the closed process $R$.
% The case in which \textsc{Tau2} is the last applied rule is analogous.
% 
% Now let \textsc{Act1} be the last rule applied. 
% Then $P \equiv P_1 \parallel P_2$ and $P' \equiv P_1' \parallel P_2$. 
% The thesis follows by applying the inductive hypothesis on $P_1$.
% The case in which \textsc{Act2} is the last applied rule is analogous.
\qed
\end{proof}

\begin{remark}\label{rem:closed}
% Notice that if we consider closed processes and 
% restrict ourselves to 
% reductions then $\fv \alpha \cap  \bv{ P_2}$ 
% ---the side condition in rules \textsc{Act1} and \textsc{Act2} in the LTS in Figure \ref{fig:ltswithalpha}--- 
% is always equivalent to the empty set. This means that $\alpha$-conversion is not necessary for closed processes.
Notice that since in \hof there is no restriction
the only binder in the language is the input prefix. 
Therefore, within a closed process $P$, the only non closed processes in $P$ are those occurring
behind an input prefix, where they cannot evolve.
By considering closed processes and restricting ourselves to 
reductions then $\alpha$-conversion is not necessary.
\end{remark}

% In order to apply the WSTS theory we need to consider a finitely branching  LTS.
% The LTS of figure \ref{fig:ltswithalpha}, because of the $\alpha$-conversion introduced in rule \textsc{ACT} is not finitely branching. Nevertheless as just observed sincein rder to prove that termination is decidable  we are only interested in closed process and reduction semantics we can consider the following LTS :

As before, the internal runs of a process are given by sequences of \emph{reductions}.
Given a process $P$, its reductions in the alternative LTS $P \newarr P'$ are defined as $P \newarro{\tau} P'$.
%the sequences of $\tau$ label transitions. 
We denote with $\newarr^*$ the reflexive and transitive closure of $\newarr$. %; notation  $\newarr^j$ is to stand for a sequence of $j$ reductions.
We use $P \not \newarr$ to denote that there is no $P'$ such  that $P \newarr P'$. 

Given a process $P$, we shall use  $P_{\alpha}$ to denote the result of applying 
the standard alpha-conversion without name captures over $P$.
%$P$ after alpha-conversion without name captures in the standard sense.

\begin{lemma}\label{lem:newlts}
 Let $P$ be a closed \hof process. %For every $P', P'' \in \hof$, 
Then, 
$P \arro{~~} P'$ iff $P \newarr P''$ and $P'' \equiv P'_\alpha$, % where $P'_\alpha$ is a possibly alpha converted version of $P'$.   
for some $P'$ in \hof.
\end{lemma}
\begin{proof}
The ``if'' direction follows easily from Remark \ref{rem:closed}.
The ``only if'' direction 
is straightforward by observing that since $P$ is a closed process, $P''$ is 
 one of the possible evolutions of $P$ in $\arro{~~}$.
%A Suppose $P \rightarrow P'$ then the thesis easily follows. (see Remark \ref{rem:closed}).
% Similarly if $P \newarr P''$ then the thesis is straightforward by observing that since $P$ is a closed process, $P''$ is one of the possible evolutions of $P$ in $\rightarrow$.
\qed
\end{proof}

\begin{corollary}
 Let $P$ be a closed \hof process. 
If $P \newarr P'$ then  $P'$ is a closed process in \hof.
%For all $P' \in \hof$, i
\end{corollary}
\begin{proof}
Straightforward from Lemma \ref{lem:close} and Lemma \ref{lem:newlts}.
\qed
\end{proof}

\begin{corollary}\label{c:termination}
 Let $P$ be a closed \hof process. $P \nrightarrow$ iff $P \not \newarr$.
\end{corollary}
\begin{proof}
 Straightforward from Lemma \ref{lem:newlts}.
\qed
\end{proof}

\begin{remark}
The encoding of a Minsky machine 
presented in Section \ref{s:turing} is a closed process.
Hence, 
%of the previous section is a closed process hence 
all the results 
in that section hold for the LTS in Figure \ref{fig:newlts} as well.
%can be proved for the new LTS.
\end{remark}



The \emph{alphabet} of an \hof process is defined as follows:

\begin{definition}[Alphabet of a process]\label{def:alpha}
Let $P$ be a \hof process. The \emph{alphabet of $P$}, denoted $\mathcal{A}(P)$, is inductively defined as:
%{\small
$$
 \mathcal{A}(\nil) = \emptyset \qquad  \qquad
 \mathcal{A}(P \parallel Q) = \mathcal{A}(P) \cup \mathcal{A}(Q) \qquad \qquad
 \mathcal{A}(x) = \{x \}
$$
$$
 \mathcal{A}(a(x).P) = \{a, x\} \cup \mathcal{A}(P) \qquad \qquad \mathcal{A}(\Ho{a}{P}) = \{a\} \cup \mathcal{A}(P)
$$
%}
\end{definition}

%RICORDARE CHE SONO TUTTI PROCESSI CHIUSI 
\shortv{
\begin{proposition}\label{prop:alpha}
Let $P$ be a \hof process. The set $\mathcal{A}(P)$ is finite.
Also, if $P \arro{\alpha} P'$ then $\mathcal{A}(P') \subseteq \mathcal{A}(P)$.
\end{proposition}}


\longv{

% {\bf CONTROLLARE COMMENTO: MA QUESTA NON E' UN OVVIETA'? A(P) È UN INDUZIONE SU UN OGGETTO SINTATTICAMENTE FINITO L'ALFABETO DEVE ESSERE FINITO, L'ALPHA CONVERSIONE DOVREBBE ENTRARE IN GIOCO SOLO NEL TEOREMA IN CUI DICIAMO CHE SE P FA UN PASSO ALLORA L'ALFABETO NON CRESCE }
% \begin{proposition}\label{prop:alpha}
% Let $P$ be a \hof process. The set $\mathcal{A}(P)$ is finite.
% \end{proposition}

% \begin{proof}
%  Straightforward  from Definition \ref{def:alpha}, exploiting the fact that in \hof alpha-conversion is not necessary %(see Remark \ref{r:alpha}).
% \qed
% \end{proof}

The following proposition can be shown for the alternative LTS because it does not consider 
alpha-conversion.
As a matter of fact, had we considered open processes, we would have required $\alpha$-conversion.
In such a case, the inclusion
$\mathcal{A}(P'_2\sub{R}{x}) \subseteq \mathcal{A}(P'_2) \cup \mathcal{A}(R)$ would no longer hold.
This is because by using $\alpha$-conversion during substitution some new variables could be added to the alphabet.
%\end{remark}

\begin{proposition}
Let $P$ and $P'$ be closed  \hof processes. If $P \newarr P'$ then $\mathcal{A}(P') \subseteq \mathcal{A}(P)$.
\end{proposition}
%\shortv{\begin{proof}[Sketch]
% Straightforward by noticing
%from Definition \ref{def:alpha} and from the fact 
%that alpha-conversion is not needed. \qed
%\end{proof}}

\begin{proof}
We proceed by a case analysis on the rule used to infer $\newarr$. 
We thus have four cases:

\begin{description}
 \item[Case \textsc{Tau1}] Then  $P = P_1 \parallel P_2$
with $P_1 \newarro{\Ho{a}{R}} P'_1$ and $P_2 \newarro{a(x)} P'_2$.
Hence $P_1 \equiv \outC{a}\langle R \rangle \parallel P'_1$,
$P_2 \equiv a(x).P'_2$,
and 
$P' = P'_1 \parallel P'_2 \sub{R}{x}$.
By Definition \ref{def:alpha} we have 
that $\mathcal{A}(P_1) = \{a\} \cup  \mathcal{A}(P'_1) \cup  \mathcal{A}(R)$
and hence $\mathcal{A}(P'_1) \subseteq  \mathcal{A}(P_1)$.
Also by Definition \ref{def:alpha} we have 
$\mathcal{A}(P_2) = \{a,x\} \cup  \mathcal{A}(P'_2)$.
Now, the process $R$ is closed: therefore, during substitution, no variable can be captured.
Hence, $\alpha$-conversion is not needed, and we have 
$\mathcal{A}(P'_2\sub{R}{x}) \subseteq \mathcal{A}(P'_2) \cup \mathcal{A}(R)$.
The result then follows. 

\item[Case \textsc{Tau2}] Similarly as for \textsc{Tau1}.

\item[Case \textsc{Act1}] Then $P \equiv P_1 \parallel P_2$, $P' \equiv P'_1 \parallel P_2$, and $P_1 \newarro{\alpha} P'_1$. 
We then have $\mathcal{A}(P'_1) \subseteq \mathcal{A}(P_1)$ by using one of the above cases.
By noting that 
$\mathcal{A}(P'_1) \cup  \mathcal{A}(P_2) \subseteq \mathcal{A}(P_1) \cup \mathcal{A}(P_2)$, the thesis holds.

\item[Case \textsc{Act2}] Similarly as for \textsc{Act1}.


\end{description}
\qed
\end{proof}



}

\begin{myfact}\label{f:fb}
The LTS for \hof given in Figure \ref{fig:newlts} is finitely branching.
\end{myfact}

%{\bf ATTENZIONE MANCANO TUTTE LE CORREZIONI AL FILE TERMINATION: CORREGGERE FRECCE E DIMOSTRAZIONI TEOREMI}